1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import analysis.calculus.mean_value
src └──────────────────────────┘
8 import tactic.monotonicity
src └─────────────────┘
9
10 /-!
11 # Extending differentiability to the boundary
12
13 We investigate how differentiable functions inside a set extend to differentiable functions
14 on the boundary. For this, it suffices that the function and its derivative admit limits there.
15 A general version of this statement is given in `has_fderiv_at_boundary_of_tendsto_fderiv`.
16
17 One-dimensional versions, in which one wants to obtain differentiability at the left endpoint or
18 the right endpoint of an interval, are given in
19 `has_deriv_at_interval_left_endpoint_of_tendsto_deriv` and
20 `has_deriv_at_interval_right_endpoint_of_tendsto_deriv`. These versions are formulated in terms
21 of the one-dimensional derivative `deriv ℝ f`.
22 -/
23
24 set_option class.instance_max_depth 40
doc └──────────────────────┘
25
26 variables {E : Type*} [normed_group E] [normed_space ℝ E]
27 {F : Type*} [normed_group F] [normed_space ℝ F]
28
29 open filter set metric continuous_linear_map
30 open_locale topological_space
31 local attribute [mono] prod_mono
id └───────┘
src └───────┘
typ └───────┘
doc └──┘
32
33 /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
34 derivative converges to `0` at a point on the boundary, then `f` is differentiable there with
35 derivative `0`. This is an auxiliary statement to prove the same result for any value of the
36 derivative, in `has_fderiv_at_boundary_of_tendsto_fderiv`. -/
37 theorem has_fderiv_at_boundary_of_tendsto_fderiv_aux {f : E → F} {s : set E} {x : E}
38 (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
39 (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
40 (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 0)) :
41 has_fderiv_within_at f (0 : E →L[ℝ] F) (closure s) x :=
42 begin
43 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
44 -- one can assume without loss of generality that `x` belongs to the closure of `s`, as the
45 -- statement is empty otherwise
46 by_cases hx : x ∉ closure s,
src └───────┘ └─┘ ┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
47 { rw ← closure_closure at hx, exact has_fderiv_within_at_of_not_mem_closure hx },
src └───┘ └────┘ └────┘ ┴ ┴
typ └───┘ └────┘ └────┘ ┴ ┴
doc └───┘ └────┘ └────┘ ┴ ┴
txt └───┘ └────┘ └────┘ ┴ ┴
par └───┘ └────┘ └────┘ ┴ ┴
pid └─┘ └────┘ ┴ ┴ ┴
48 push_neg at hx,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────┘
49 /- One needs to show that `∥f y - f x∥ ≤ ε ∥y - x∥` for `y` close to `x` in `closure s`, where
50 `ε` is an arbitrary positive constant. By continuity of the functions, it suffices to prove this
51 for nearby points inside `s`. In a neighborhood of `x`, the derivative of `f` is arbitrarily small
52 by assumption. The mean value inequality ensures that `f` is `ε`-Lipschitz there, concluding the
53 proof. -/
54 assume ε ε_pos,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
55 obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ∥fderiv ℝ f y∥ < ε,
id ┴ ┴ └──┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴
src └──────────────────────┘ └────┘┴┴ └───┘ ┴└──┘┴ ┴ ┴┴┴ ┴ ┴┴└────┘┴ ┴ ┴ ┴┴ ┴
typ └──────────────────────┘ └────┘┴┴ └───┘┴ ┴└──┘┴ ┴┴┴┴┴ ┴ ┴┴└────┘┴ ┴┴┴ ┴┴ ┴┴
doc └──────────────────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ ┴ ┴
txt └──────────────────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └──────────────────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └────────────────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────────────────┘
56 by simpa [dist_zero_right] using tendsto_nhds_within_nhds.1 h ε ε_pos,
id └─────────────┘ └──────────────────────┘ ┴ ┴ └───┘
src └─────┘└─────────────┘└──────┘└──────────────────────┘└─┘ ┴ ┴
typ └─────┘└─────────────┘└──────┘└──────────────────────┘└─┘┴┴┴┴└───┘
doc └─────┘ └──────┘ └─┘ ┴ ┴
txt └─────┘ └──────┘ └─┘ ┴ ┴
par └─────┘ └──────┘ └─┘ ┴ ┴
pid ┴┴ ┴┴└────┘ └─┘ ┴ ┴
st └─
57 set B := ball x δ,
id └──┘ ┴ ┴
src └───────┘└──┘┴ ┴
typ └───────┘└──┘┴┴┴┴
doc └───────┘└──┘┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴┴┴└┘┴ ┴ ┴
st ──────────────────┘└─
58 suffices : ∀ y ∈ B ∩ (closure s), ∥f y - f x∥ ≤ ε * ∥y - x∥,
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └───┘ ┴┴┴ └─────┘┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴
typ └─────────┘ └───┘┴┴┴┴ └─────┘┴┴┴ ┴ ┴ ┴┴┴┴┴ ┴┴┴┴┴┴┴ ┴ ┴┴
doc └─────────┘ └───┘ ┴ ┴ └─────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
59 from mem_nhds_within_iff.2 ⟨δ, δ_pos, λy hy, by simpa using this y hy⟩,
id └─────────────────┘ ┴ └───┘ └──┘ ┴ └┘
src └───┘└─────────────────┘└─┘ └┘ └┘ └────┘ ┴└──────────┘ ┴ ┴ ┴
typ └───┘└─────────────────┘└─┘ ┴└┘└───┘└┘ └────┘ ┴└──────────┘└──┘┴┴┴└┘┴
doc └───┘ └─┘ └┘ └┘ └────┘ ┴└──────────┘ ┴ ┴ ┴
txt └───┘ └─┘ └┘ └┘ └────┘ ┴└──────────┘ ┴ ┴ ┴
par └───┘ └─┘ └┘ └┘ └────┘ ┴└──────────┘ ┴ ┴ ┴
pid └───┘ └─┘ └┘ └┘ └────┘ └───────────┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────┘└────────────────────┘┴└─
60 suffices : ∀ p : E × E, p ∈ closure ((B ∩ s).prod (B ∩ s)) → ∥f p.2 - f p.1∥ ≤ ε * ∥p.2 - p.1∥,
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─────────┘ └───┘ ┴┴┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
typ └─────────┘ └───┘ ┴┴┴┴ ┴ ┴┴┴└─────┘┴ ┴ ┴ └─────┘ ┴┴ ┴┴└─┘ ┴ ┴ └─┘ ┴┴┴ └┘ ┴ ┴┴┴ ┴ └─┘ ┴ └┘
doc └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
txt └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid └───────┘└┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
61 { rw closure_prod_eq at this,
id └─────────────┘
src └─┘└─────────────┘└──────┘
typ └─┘└─────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ───┘└────────────────────────┘└─
62 intros y y_in,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
63 apply this ⟨x, y⟩,
id └──┘ ┴ ┴
src └────┘ ┴ └┘ ┴
typ └────┘└──┘┴ ┴└┘┴┴
doc └────┘ ┴ └┘ ┴
txt └────┘ ┴ └┘ ┴
par └────┘ ┴ └┘ ┴
pid ┴ ┴ └┘ ┴
st ────────────────────┘└─
64 have : B ∩ closure s ⊆ closure (B ∩ s), from closure_inter_open is_open_ball,
id ┴ └─────┘ ┴ ┴ └────────────────┘ └──────────┘
src └─────┘ ┴ ┴ ┴ ┴┴┴└─────┘┴ ┴ ┴ ┴ └───┘└────────────────┘┴└──────────┘
typ └─────┘ ┴ ┴ ┴ ┴┴┴└─────┘┴ ┴┴ ┴┴┴ └───┘└────────────────┘┴└──────────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ ┴ └───┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
st ─────────────────────────────────────────┘└────────────────────────────────────┘└─
65 exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩ },
id └───────────┘ └───┘ └┘ └──┘ └──┘
src └────┘ ┴ └───────────┘┴ └┘ └─┘ ┴ └┘
typ └────┘ ┴ └───────────┘┴└───┘└┘└┘└─┘└──┘┴└──┘└┘
doc └────┘ ┴ ┴ └┘ └─┘ ┴ └┘
txt └────┘ ┴ ┴ └┘ └─┘ ┴ └┘
par └────┘ ┴ ┴ └┘ └─┘ ┴ └┘
pid ┴ ┴ ┴ └┘ └─┘ ┴ ┴┴
st ─────────────────────────────────────────────────────┘└┘└
66 have key : ∀ p : E × E, p ∈ (B ∩ s).prod (B ∩ s) → ∥f p.2 - f p.1∥ ≤ ε * ∥p.2 - p.1∥,
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
typ └─────────┘ └───┘ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ └─────┘ ┴┴ ┴┴└┘ ┴ ┴ └─┘ ┴┴┴ └┘ ┴ ┴┴┴ ┴ └─┘ ┴ └┘
doc └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
txt └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid └──────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
67 { rintros ⟨u, v⟩ ⟨u_in, v_in⟩,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └──────────────────┘
st ───┘└─────────────────────────┘└─
68 have conv : convex (B ∩ s) := (convex_ball _ _).inter s_conv,
id └────┘ ┴ ┴ └─────────┘ └────┘
src └──────────┘└────┘┴ ┴ ┴ └───┘ └─────────┘└──────────┘
typ └──────────┘└────┘┴ ┴┴ ┴┴└───┘ └─────────┘└──────────┘└────┘
doc └──────────┘└────┘┴ ┴ ┴ └───┘ └──────────┘
txt └──────────┘ ┴ ┴ ┴ └───┘ └──────────┘
par └──────────┘ ┴ ┴ ┴ └───┘ └──────────┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴└──┘ └──────────┘
st ───────────────────────────────────────────────────────────────┘└─
69 have diff : differentiable_on ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _),
id └───────────────┘ ┴ ┴ ┴ └─────────┘ └────────────────┘
src └──────────┘└───────────────┘┴ ┴ ┴ ┴ ┴ └───┘└─────────┘┴ └────────────────┘└───┘
typ └──────────┘└───────────────┘┴ ┴┴┴ ┴┴ ┴┴└───┘└─────────┘┴ └────────────────┘└───┘
doc └──────────┘└───────────────┘┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └───┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
70 refine conv.norm_image_sub_le_of_norm_deriv_le diff (λz z_in, _) u_in v_in,
id └─────────────────────────────────────┘ └──┘ └──┘ └──┘
src └─────┘└─────────────────────────────────────┘┴ ┴ └─────────┘ ┴
typ └─────┘└─────────────────────────────────────┘┴└──┘┴ └─────────┘└──┘┴└──┘
doc └─────┘└─────────────────────────────────────┘┴ ┴ └─────────┘ ┴
txt └─────┘ ┴ ┴ └─────────┘ ┴
par └─────┘ ┴ ┴ └─────────┘ ┴
pid ┴ ┴ ┴ └─────────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└─
71 convert le_of_lt (hδ _ z_in.2 z_in.1),
id └──────┘ └┘ └──┘
src └──────┘└──────┘┴ └─┘ └─┘ └─┘
typ └──────┘└──────┘┴ └┘└─┘ └─┘└──┘└─┘
doc └──────┘ ┴ └─┘ └─┘ └─┘
txt └──────┘ ┴ └─┘ └─┘ └─┘
par └──────┘ ┴ └─┘ └─┘ └─┘
pid ┴ ┴ └─┘ └─┘ └─┘
st ────────────────────────────────────────┘└─
72 have op : is_open (B ∩ s) := is_open_inter is_open_ball s_open,
id └─────┘ ┴ ┴ └───────────┘ └──────────┘ └────┘
src └────────┘└─────┘┴ ┴ ┴ └───┘└───────────┘┴└──────────┘┴
typ └────────┘└─────┘┴ ┴┴ ┴┴└───┘└───────────┘┴└──────────┘┴└────┘
doc └────────┘└─────┘┴ ┴ ┴ └───┘ ┴ ┴
txt └────────┘ ┴ ┴ ┴ └───┘ ┴ ┴
par └────────┘ ┴ ┴ ┴ └───┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└─
73 rw differentiable_at.fderiv_within _ (op.unique_diff_on z z_in),
id └─────────────────────────────┘ └───────────────┘ ┴ └──┘
src └─┘└─────────────────────────────┘└─┘ └───────────────┘┴ ┴ ┴
typ └─┘└─────────────────────────────┘└─┘ └───────────────┘┴┴┴└──┘┴
doc └─┘ └─┘ ┴ ┴ ┴
txt └─┘ └─┘ ┴ ┴ ┴
par └─┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────┘└─
74 exact (diff z z_in).differentiable_at (mem_nhds_sets op z_in) },
id └──┘ ┴ └───────────┘ └┘ └──┘
src └────┘ ┴ ┴ └──────────────────┘ └───────────┘┴ ┴ └┘
typ └────┘ └──┘┴┴┴ └──────────────────┘ └───────────┘┴└┘┴└──┘└┘
doc └────┘ ┴ ┴ └──────────────────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └──────────────────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └──────────────────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────┘└┘└
75 rintros ⟨u, v⟩ uv_in,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ─────────────────────┘└─
76 refine continuous_within_at.closure_le uv_in _ _ key,
id └─────────────────────────────┘ └───┘ └─┘
src └─────┘└─────────────────────────────┘┴ └───┘
typ └─────┘└─────────────────────────────┘┴└───┘└───┘└─┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────────────────────────────────┘└─
77 all_goals { -- common start for both continuity proofs
src └──────────────────────────────────────────────────────
typ └──────────────────────────────────────────────────────
doc └──────────────────────────────────────────────────────
txt └──────────────────────────────────────────────────────
par └──────────────────────────────────────────────────────
pid └─────────────────────────────────────────────
st ────────────┘└───────────────────────────────────────────
78 have : (B ∩ s).prod (B ∩ s) ⊆ s.prod s, by mono ; exact inter_subset_right _ _,
id ┴ └────┘ ┴ └────────────────┘
src ───┘└─────┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴└────┘┴ └───┘└───┘└┘└────┘└────────────────┘└──┘└─
typ ───┘└─────┘ ┴ ┴ └─────┘ ┴┴ ┴ └┘ ┴└────┘┴┴└───┘└───┘└┘└────┘└────────────────┘└──┘└─
doc ───┘└─────┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴└────┘┴ └───┘└───┘└┘└────┘ └──┘└─
txt ───┘└─────┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └───┘└───┘└┘└────┘ └──┘└─
par ───┘└─────┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └───┘└───┘└┘└────┘ └──┘└─
pid ──────────┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ └────────────────┘ └─────
st ─────────────────────────────────────────┘ └─
79 obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s,
id ┴ ┴ └─────┘ ┴
src ───┘└────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────┘┴ └─
typ ───┘└────────────────────┘┴┴ ┴ ┴ ┴ ┴┴┴ ┴└─────┘┴┴└─
doc ───┘└────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────┘┴ └─
txt ───┘└────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───┘└────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────┘
80 by simpa [closure_prod_eq] using closure_mono this uv_in,
id └─────────────┘ └──────────┘ └──┘ └───┘
src ────────┘└─────┘└─────────────┘└──────┘└──────────┘┴ ┴ └─
typ ────────┘└─────┘└─────────────┘└──────┘└──────────┘┴└──┘┴└───┘└─
doc ────────┘└─────┘ └──────┘ ┴ ┴ └─
txt ────────┘└─────┘ └──────┘ ┴ ┴ └─
par ────────┘└─────┘ └──────┘ ┴ ┴ └─
pid ───────────────┘ └──────┘ ┴ ┴ └─
st └─
81 apply continuous_within_at.mono _ this,
id └───────────────────────┘ └──┘
src ───┘└────┘└───────────────────────┘└─┘ └─
typ ───┘└────┘└───────────────────────┘└─┘└──┘└─
doc ───┘└────┘ └─┘ └─
txt ───┘└────┘ └─┘ └─
par ───┘└────┘ └─┘ └─
pid ─────────┘ └─┘ └─
st ─────────────────────────────────────────┘└─
82 simp only [continuous_within_at, nhds_prod_eq] },
id └──────────────────┘ └──────────┘
src ───┘└─────────┘└──────────────────┘└┘└──────────┘└┘┴
typ ───┘└─────────┘└──────────────────┘└┘└──────────┘└┘┴
doc ───┘└─────────┘└──────────────────┘└┘ └┘┴
txt ───┘└─────────┘ └┘ └┘┴
par ───┘└─────────┘ └┘ └┘┴
pid ──────────────┘ └┘ └─┘
st ──────────────────────────────────────────────────┘└┘└
83 { rw nhds_within_prod_eq,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└────────────────────┘└─
84 exact tendsto.comp continuous_norm.continuous_at
id └───────────────────────────┘
src └────┘ ┴└───────────────────────────┘└
typ └────┘ ┴└───────────────────────────┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ─────────────────────────────────────────────────────
85 ((tendsto.comp (f_cont v v_in) tendsto_snd).sub $ tendsto.comp (f_cont u u_in) tendsto_fst) },
id ┴ └──┘ └─────────┘ └──────────┘ └────┘ ┴ └──┘ └─────────┘
src ─────┘ ┴ ┴ ┴ └┘└─────────┘└────┘ ┴└──────────┘┴ ┴ ┴ └┘└─────────┘└┘
typ ─────┘ ┴ ┴┴┴└──┘└┘└─────────┘└────┘ ┴└──────────┘┴ └────┘┴┴┴└──┘└┘└─────────┘└┘
doc ─────┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ └┘ └┘
txt ─────┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ └┘ └┘
par ─────┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ └┘ └┘
pid ─────┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
86 { apply tendsto_nhds_within_of_tendsto_nhds,
id └─────────────────────────────────┘
src └────┘└─────────────────────────────────┘
typ └────┘└─────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────────────────┘└─
87 rw nhds_prod_eq,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
88 exact tendsto_const_nhds.mul
id └────────────────────┘
src └────┘└────────────────────┘└
typ └────┘└────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────────────
89 (tendsto.comp continuous_norm.continuous_at $ tendsto_snd.sub tendsto_fst) },
id └──────────┘ └───────────────────────────┘ └─────────────┘ └─────────┘
src ─────┘ └──────────┘┴└───────────────────────────┘┴ ┴└─────────────┘┴└─────────┘└┘
typ ─────┘ └──────────┘┴└───────────────────────────┘┴ ┴└─────────────┘┴└─────────┘└┘
doc ─────┘ ┴ ┴ ┴ ┴ └┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘
par ─────┘ ┴ ┴ ┴ ┴ └┘
pid ─────┘ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────┘└──
90 end
st ──┘
91
92 /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
93 derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
94 with derivative `f'`. -/
95 theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : set E} {x : E} {f' : E →L[ℝ] F}
id ┴ ┴ └─┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └─┘ └─┘┴┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └─┘ ┴
96 (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
id └───────────────┘ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴
src └───────────────┘ ┴ └────┘ └─────┘
typ └───────────────┘ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴
doc └───────────────┘ └────┘ └─────┘
97 (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
id ┴ └─────┘ ┴ └──────────────────┘ ┴ ┴ ┴
src └─────┘ └──────────────────┘
typ ┴ └─────┘ ┴ └──────────────────┘ ┴ ┴ ┴
doc └─────┘ └──────────────────┘
98 (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 f')) :
id └─────┘ ┴ └────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └┘
src └─────┘ └────┘ ┴ └─────────┘ ┴
typ └─────┘ ┴ └────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └┘
doc └─────┘ └────┘ └─────────┘ ┴
99 has_fderiv_within_at f f' (closure s) x :=
id └──────────────────┘ ┴ └┘ └─────┘ ┴ ┴
src └──────────────────┘ └─────┘
typ └──────────────────┘ ┴ └┘ └─────┘ ┴ ┴
doc └──────────────────┘ └─────┘
100 begin
st └─────
101 /- We subtract `f'` to define a new function `g` for which `g' = 0`, for which differentiability
st ───────────────────────────────────────────────────────────────────────────────────────────────────
102 is proved `has_fderiv_at_boundary_of_differentiable_aux`. Then, we just need to glue together the
st ────────────────────────────────────────────────────────────────────────────────────────────────────
103 pieces, expressing back `f` in terms of `g`. -/
st ──────────────────────────────────────────────────
104 let g := λy, f y - f' y,
id ┴ ┴ └┘
src └───────┘ └─┘ ┴ ┴┴┴ ┴
typ └───────┘ └─┘┴┴ ┴┴┴└┘┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └─┘ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
105 have diff_g : differentiable_on ℝ g s :=
id └───────────────┘ ┴ ┴
src └────────────┘└───────────────┘┴ ┴ ┴ └───
typ └────────────┘└───────────────┘┴ ┴┴┴┴└───
doc └────────────┘└───────────────┘┴ ┴ ┴ └───
txt └────────────┘ ┴ ┴ ┴ └───
par └────────────┘ ┴ ┴ ┴ └───
pid └─────────┘└─┘ ┴ ┴ ┴ └───
st ───────────────────────────────────────────
106 f_diff.sub (f'.differentiable.comp differentiable_id).differentiable_on,
id └────────┘ └────────────────────┘ └───────────────┘
src ───┘└────────┘┴ └────────────────────┘┴└───────────────┘└─────────────────┘
typ ───┘└────────┘┴ └────────────────────┘┴└───────────────┘└─────────────────┘
doc ───┘ ┴ ┴ └─────────────────┘
txt ───┘ ┴ ┴ └─────────────────┘
par ───┘ ┴ ┴ └─────────────────┘
pid ───┘ ┴ ┴ └────────────────┘┴
st ──────────────────────────────────────────────────────────────────────────┘└─
107 have cont_g : ∀y ∈ closure s, continuous_within_at g s y :=
id └─────┘ └──────────────────┘ ┴ ┴
src └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴ └───
typ └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴┴┴┴┴ └───
doc └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴ └───
txt └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ └───
par └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ └───
pid └─────────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────
108 λy hy, tendsto.sub (f_cont y hy) (f'.continuous.comp continuous_id).continuous_within_at,
id └─────────┘ └────┘ └────────────────┘ └───────────┘
src ───┘ └────┘└─────────┘┴ ┴ ┴ └┘ └────────────────┘┴└───────────┘└────────────────────┘
typ ───┘ └────┘└─────────┘┴ └────┘┴ ┴ └┘ └────────────────┘┴└───────────┘└────────────────────┘
doc ───┘ └────┘ ┴ ┴ ┴ └┘ ┴ └────────────────────┘
txt ───┘ └────┘ ┴ ┴ ┴ └┘ ┴ └────────────────────┘
par ───┘ └────┘ ┴ ┴ ┴ └┘ ┴ └────────────────────┘
pid ───┘ └────┘ ┴ ┴ ┴ └┘ ┴ └───────────────────┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
109 have A : ∀y ∈ s, fderiv ℝ f y - f' = fderiv ℝ g y,
id ┴ ┴ └┘ ┴ └────┘ ┴
src └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴└────┘┴ ┴ ┴
typ └───────┘ └──┘┴ ┴ ┴ ┴┴┴ ┴ ┴└┘┴┴┴└────┘┴ ┴┴┴
doc └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘┴ ┴ ┴
txt └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────┘└─
110 { assume y hy,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
111 have : has_fderiv_at f (fderiv ℝ f y) y :=
id └───────────┘ └────┘ ┴ ┴
src └─────┘└───────────┘┴ ┴ └────┘┴ ┴ ┴ └┘ └───
typ └─────┘└───────────┘┴ ┴ └────┘┴ ┴┴┴ └┘┴└───
doc └─────┘└───────────┘┴ ┴ └────┘┴ ┴ ┴ └┘ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
st ───────────────────────────────────────────────
112 (differentiable_within_at.differentiable_at (f_diff y hy) (mem_nhds_sets s_open hy)).has_fderiv_at,
id └────────────────────────────────────────┘ └────┘ ┴ └───────────┘ └────┘ └┘
src ─────┘ └────────────────────────────────────────┘┴ ┴ ┴ └┘ └───────────┘┴ ┴ └──────────────┘
typ ─────┘ └────────────────────────────────────────┘┴ └────┘┴┴┴ └┘ └───────────┘┴└────┘┴└┘└──────────────┘
doc ─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘
txt ─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘
par ─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘
pid ─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
113 have : has_fderiv_at g (fderiv ℝ f y - f') y :=
id └───────────┘ ┴ └────┘ ┴ └┘ ┴
src └─────┘└───────────┘┴ ┴ └────┘┴ ┴ ┴ ┴ ┴ └┘ └───
typ └─────┘└───────────┘┴┴┴ └────┘┴ ┴┴┴ ┴ ┴└┘└┘┴└───
doc └─────┘└───────────┘┴ ┴ └────┘┴ ┴ ┴ ┴ ┴ └┘ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
st ────────────────────────────────────────────────────
114 this.sub (f'.has_fderiv_at.comp y (has_fderiv_at_id y)),
id └──────┘ └───────────────────┘ └──────────────┘ ┴
src ─────┘└──────┘┴ └───────────────────┘┴ ┴ └──────────────┘┴ └┘
typ ─────┘└──────┘┴ └───────────────────┘┴ ┴ └──────────────┘┴┴└┘
doc ─────┘ ┴ └───────────────────┘┴ ┴ ┴ └┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘
par ─────┘ ┴ ┴ ┴ ┴ └┘
pid ─────┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────┘└─
115 exact this.fderiv.symm },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└┘└
116 have B : tendsto (λy, fderiv ℝ f y - f') (nhds_within x s) (𝓝 (f' - f')) :=
id └─────┘ └────┘ ┴ └─────────┘ ┴ ┴ ┴ └┘
src └───────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ ┴ ┴ └─────
typ └───────┘└─────┘┴ └─┘└────┘┴ ┴┴┴ ┴ ┴ └┘ └─────────┘┴┴┴┴└┘ ┴┴ ┴ ┴└┘└─────
doc └───────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ ┴ ┴ └─────
txt └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────
par └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────
pid └────┘└─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───
st ──────────────────────────────────────────────────────────────────────────────
117 h.sub tendsto_const_nhds,
id └───┘ └────────────────┘
src ───┘└───┘┴└────────────────┘
typ ───┘└───┘┴└────────────────┘
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ───────────────────────────┘└─
118 have : tendsto (λy, fderiv ℝ g y) (nhds_within x s) (𝓝 0),
id └─────┘ └────┘ ┴ └─────────┘ ┴ ┴
src └─────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ └─┘
typ └─────┘└─────┘┴ └─┘└────┘┴ ┴┴┴ └┘ └─────────┘┴┴┴┴└┘ └─┘
doc └─────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ └─┘
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘
st ──────────────────────────────────────────────────────────┘└─
119 { have : f' - f' = 0, by simp,
id └┘
src └─────┘ ┴ ┴ ┴ └┘ └──┘
typ └─────┘ ┴ ┴└┘┴ └┘ └──┘
doc └─────┘ ┴ ┴ ┴ └┘ └──┘
txt └─────┘ ┴ ┴ ┴ └┘ └──┘
par └─────┘ ┴ ┴ ┴ └┘ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴┴
st ───┘└────────────────┘ └─
120 rw this at B,
id └──┘
src └─┘ └───┘
typ └─┘└──┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────┘└─
121 apply tendsto.congr' _ B,
id └────────────┘ ┴
src └────┘└────────────┘└─┘
typ └────┘└────────────┘└─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───────────────────────────┘└─
122 filter_upwards [self_mem_nhds_within] A },
id └──────────────────┘ ┴
src └──────────────┘└──────────────────┘└┘ ┴
typ └──────────────┘└──────────────────┘└┘┴┴
doc └──────────────┘ └┘ ┴
txt └──────────────┘ └┘ ┴
par └──────────────┘ └┘ ┴
pid └┘ ┴┴ ┴
st ───────────────────────────────────────────┘└┘└
123 have : has_fderiv_within_at g (0 : E →L[ℝ] F) (closure s) x :=
id └──────────────────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘└──────────────────┘┴ ┴ └──┘ ┴└─┘ ┴┴ └┘ └─────┘┴ └┘ └───
typ └─────┘└──────────────────┘┴┴┴ └──┘┴┴└─┘ ┴┴┴└┘ └─────┘┴┴└┘┴└───
doc └─────┘└──────────────────┘┴ ┴ └──┘ ┴└─┘ ┴┴ └┘ └─────┘┴ └┘ └───
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └───
par └─────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └───
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └───
st ─────────────────────────────────────────────────────────────────
124 has_fderiv_at_boundary_of_tendsto_fderiv_aux diff_g s_conv s_open cont_g this,
id └──────────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └──┘
src ───┘└──────────────────────────────────────────┘┴ ┴ ┴ ┴ ┴
typ ───┘└──────────────────────────────────────────┘┴└────┘┴└────┘┴└────┘┴└────┘┴└──┘
doc ───┘└──────────────────────────────────────────┘┴ ┴ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
125 convert this.add f'.has_fderiv_within_at,
id └──────┘ └─────────────────────┘
src └──────┘└──────┘┴└─────────────────────┘
typ └──────┘└──────┘┴└─────────────────────┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────────┘└─
126 { ext y, simp [g] },
id ┴
src └───┘ └────┘ └┘
typ └───┘ └────┘┴└┘
doc └───┘ └────┘ └┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st ───┘└───┘└─────────┘└┘└
127 { simp }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
128 end
st ──┘
129
130 /-- If a function is differentiable on the right of a point `a : ℝ`, continuous at `a`, and
131 its derivative also converges at `a`, then `f` is differentiable on the right at `a`. -/
132 lemma has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
133 (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
id └───────────────┘ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
src └───────────────┘ ┴ └──────────────────┘
typ └───────────────┘ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
doc └───────────────┘ └──────────────────┘
134 (hs : s ∈ nhds_within a (Ioi a))
id ┴ ┴ └─────────┘ ┴ └─┘ ┴
src ┴ └─────────┘ └─┘
typ ┴ ┴ └─────────┘ ┴ └─┘ ┴
doc └─────────┘ └─┘
135 (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Ioi a)) (𝓝 e)) :
id └─────┘ ┴ └───┘ ┴ ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ └───┘ └─────────┘ └─┘ ┴
typ └─────┘ ┴ └───┘ ┴ ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴
doc └─────┘ └───┘ └─────────┘ └─┘ ┴
136 has_deriv_within_at f e (Ici a) a :=
id └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
src └─────────────────┘ └─┘
typ └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
doc └─────────────────┘ └─┘
137 begin
st └─────
138 /- This is a specialization of `has_fderiv_at_boundary_of_tendsto_fderiv`. To be in the setting of
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
139 this theorem, we need to work on an open interval with closure contained in `s ∪ {a}`, that we
st ─────────────────────────────────────────────────────────────────────────────────────────────────
140 call `t = (a, b)`. Then, we check all the assumptions of this theorem and we apply it. -/
st ────────────────────────────────────────────────────────────────────────────────────────────
141 obtain ⟨b, ab, sab⟩ : ∃ b ∈ Ioi a, Ioc a b ⊆ s :=
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └────────────────────┘┴└───┘└─┘┴ ┴┴└─┘┴ ┴ ┴┴┴ └───
typ └────────────────────┘┴└───┘└─┘┴ ┴┴└─┘┴┴┴ ┴┴┴┴└───
doc └────────────────────┘ └───┘└─┘┴ ┴└─┘┴ ┴ ┴ ┴ └───
txt └────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └──────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────────────────
142 mem_nhds_within_Ioi_iff_exists_Ioc_subset.1 hs,
id └───────────────────────────────────────┘ └┘
src ───┘└───────────────────────────────────────┘└─┘
typ ───┘└───────────────────────────────────────┘└─┘└┘
doc ───┘└───────────────────────────────────────┘└─┘
txt ───┘ └─┘
par ───┘ └─┘
pid ───┘ └─┘
st ─────────────────────────────────────────────────┘└─
143 let t := Ioo a b,
id └─┘ ┴ ┴
src └───────┘└─┘┴ ┴
typ └───────┘└─┘┴┴┴┴
doc └───────┘└─┘┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴
st ─────────────────┘└─
144 have ts : t ⊆ s := subset.trans Ioo_subset_Ioc_self sab,
id ┴ ┴ └──────────┘ └─────────────────┘ └─┘
src └────────┘ ┴ ┴ └──┘└──────────┘┴└─────────────────┘┴
typ └────────┘┴┴ ┴┴└──┘└──────────┘┴└─────────────────┘┴└─┘
doc └────────┘ ┴ ┴ └──┘ ┴ ┴
txt └────────┘ ┴ ┴ └──┘ ┴ ┴
par └────────┘ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
145 have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
id └───────────────┘ ┴ ┴ └─────────┘ └┘
src └────────────┘└───────────────┘┴ ┴ ┴ └──┘└─────────┘┴
typ └────────────┘└───────────────┘┴ ┴┴┴┴└──┘└─────────┘┴└┘
doc └────────────┘└───────────────┘┴ ┴ ┴ └──┘ ┴
txt └────────────┘ ┴ ┴ ┴ └──┘ ┴
par └────────────┘ ┴ ┴ ┴ └──┘ ┴
pid └─────────┘└─┘ ┴ ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────┘└─
146 have t_conv : convex t := convex_Ioo a b,
id └────┘ ┴ └────────┘ ┴ ┴
src └────────────┘└────┘┴ └──┘└────────┘┴ ┴
typ └────────────┘└────┘┴┴└──┘└────────┘┴┴┴┴
doc └────────────┘└────┘┴ └──┘ ┴ ┴
txt └────────────┘ ┴ └──┘ ┴ ┴
par └────────────┘ ┴ └──┘ ┴ ┴
pid └─────────┘└─┘ ┴ └──┘ ┴ ┴
st ─────────────────────────────────────────┘└─
147 have t_open : is_open t := is_open_Ioo,
id └─────┘ ┴ └─────────┘
src └────────────┘└─────┘┴ └──┘└─────────┘
typ └────────────┘└─────┘┴┴└──┘└─────────┘
doc └────────────┘└─────┘┴ └──┘
txt └────────────┘ ┴ └──┘
par └────────────┘ ┴ └──┘
pid └─────────┘└─┘ ┴ └──┘
st ───────────────────────────────────────┘└─
148 have t_closure : closure t = Icc a b := closure_Ioo ab,
id └─────┘ ┴ ┴ └─┘ ┴ ┴ └─────────┘ └┘
src └───────────────┘└─────┘┴ ┴┴┴└─┘┴ ┴ └──┘└─────────┘┴
typ └───────────────┘└─────┘┴┴┴┴┴└─┘┴┴┴┴└──┘└─────────┘┴└┘
doc └───────────────┘└─────┘┴ ┴ ┴└─┘┴ ┴ └──┘└─────────┘┴
txt └───────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────────────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────┘└─
149 have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
id └─────┘ └──────────────────┘ ┴ ┴
src └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴
typ └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴┴┴┴┴
doc └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴
txt └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴
par └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴
pid └─────────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
150 { rw t_closure,
id └───────┘
src └─┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└──────────┘└─
151 assume y hy,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
152 by_cases h : y = a,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
153 { rw h, exact f_lim.mono ts },
id ┴ └────────┘ └┘
src └─┘ └────┘└────────┘┴ ┴
typ └─┘┴ └────┘└────────┘┴└┘┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└──┘└────────────────────┘└┘└
154 { have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (ne.symm h), hy.2⟩,
id ┴ ┴ └─┘ └────────────┘ └─────┘ ┴ └┘
src └─────┘ ┴ ┴ └──┘ ┴ └────────────┘┴ └─┘ └─────┘┴ └─┘ └─┘
typ └─────┘┴┴ ┴┴└──┘└─┘┴ └────────────┘┴ └─┘ └─────┘┴┴└─┘└┘└─┘
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘ └─┘
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘ └─┘
par └─────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘ └─┘
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘ └─┘
st ────────────────────────────────────────────────────────────────┘└─
155 exact (f_diff.continuous_on y this).mono ts } },
id └──────────────────┘ ┴ └──┘ └┘
src └────┘ └──────────────────┘┴ ┴ └─────┘ ┴
typ └────┘ └──────────────────┘┴┴┴└──┘└─────┘└┘┴
doc └────┘ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ └─────┘ ┴
st ─────────────────────────────────────────────────┘└──┘└
156 have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
id └─────┘ └────┘ ┴ └─────────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ └────────┘└─┘ └┘
typ └─────────────┘└─────┘┴ └─┘└────┘┴ ┴┴┴ └┘ └─────────┘┴┴┴┴└┘ ┴┴ └────────┘└─┘┴└┘
doc └─────────────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ └────────┘└─┘ └┘
txt └─────────────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
par └─────────────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
pid └──────────┘└─┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
st ─────────────────────────────────────────────────────────────────────────────────┘└─
157 { simp [deriv_fderiv.symm],
src └────┘ ┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───┘└──────────────────────┘└─
158 refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
id └──────────┘ └───────────────────────────────────────────────────────────────┘
src └─────┘└──────────┘┴└───────────────────────────────────────────────────────────────┘└┘
typ └─────┘└──────────┘┴└───────────────────────────────────────────────────────────────┘└┘
doc └─────┘ ┴└───────────────────────────────────────────────────────────────┘└┘
txt └─────┘ ┴ └┘
par └─────┘ ┴ └┘
pid ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
159 exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' },
id └─────────────┘ └──────────────┘ └─────────────────┘ └────┘
src └────┘└─────────────┘┴ └──────────────┘└─┘└─────────────────┘└┘ ┴
typ └────┘└─────────────┘┴ └──────────────┘└─┘└─────────────────┘└┘└────┘┴
doc └────┘ ┴ └─┘ └┘ ┴
txt └────┘ ┴ └─┘ └┘ ┴
par └────┘ ┴ └─┘ └┘ ┴
pid ┴ ┴ └─┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
160 -- now we can apply `has_fderiv_at_boundary_of_differentiable`
st ─────────────────────────────────────────────────────────────────
161 have : has_deriv_within_at f e (Icc a b) a,
id └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
src └─────┘└─────────────────┘┴ ┴ ┴ └─┘┴ ┴ └┘
typ └─────┘└─────────────────┘┴┴┴┴┴ └─┘┴ ┴┴└┘┴
doc └─────┘└─────────────────┘┴ ┴ ┴ └─┘┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
162 { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],
id └──────────────────────────────────────────┘ └───────┘
src └──┘└──────────────────────────────────────────┘└──┘ ┴
typ └──┘└──────────────────────────────────────────┘└──┘└───────┘┴
doc └──┘└──────────────────────────────────────────┘└──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ───┘└──────────────────────────────────────────────┘└───────────┘└──
163 exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff' },
id └──────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └─────┘
src └────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴
typ └────┘└──────────────────────────────────────┘┴└────┘┴└────┘┴└────┘┴└────┘┴└─────┘┴
doc └────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└┘└
164 exact this.nhds_within (mem_nhds_within_Ici_iff_exists_Icc_subset.2 ⟨b, ab, subset.refl _⟩)
id └──────────────┘ └───────────────────────────────────────┘ ┴ └┘ └─────────┘
src └────┘└──────────────┘┴ └───────────────────────────────────────┘└─┘ └┘ └┘└─────────┘└───┘
typ └────┘└──────────────┘┴ └───────────────────────────────────────┘└─┘ ┴└┘└┘└┘└─────────┘└───┘
doc └────┘ ┴ └───────────────────────────────────────┘└─┘ └┘ └┘ └───┘
txt └────┘ ┴ └─┘ └┘ └┘ └───┘
par └────┘ ┴ └─┘ └┘ └┘ └───┘
pid ┴ ┴ └─┘ └┘ └┘ └──┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────────┘
165 end
st └─┘
166
167 /-- If a function is differentiable on the left of a point `a : ℝ`, continuous at `a`, and
168 its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
169 lemma has_fderiv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
170 (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
id └───────────────┘ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
src └───────────────┘ ┴ └──────────────────┘
typ └───────────────┘ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
doc └───────────────┘ └──────────────────┘
171 (hs : s ∈ nhds_within a (Iio a))
id ┴ ┴ └─────────┘ ┴ └─┘ ┴
src ┴ └─────────┘ └─┘
typ ┴ ┴ └─────────┘ ┴ └─┘ ┴
doc └─────────┘ └─┘
172 (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Iio a)) (𝓝 e)) :
id └─────┘ ┴ └───┘ ┴ ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ └───┘ └─────────┘ └─┘ ┴
typ └─────┘ ┴ └───┘ ┴ ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴
doc └─────┘ └───┘ └─────────┘ └─┘ ┴
173 has_deriv_within_at f e (Iic a) a :=
id └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
src └─────────────────┘ └─┘
typ └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
doc └─────────────────┘ └─┘
174 begin
st └─────
175 /- This is a specialization of `has_fderiv_at_boundary_of_differentiable`. To be in the setting of
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
176 this theorem, we need to work on an open interval with closure contained in `s ∪ {a}`, that we
st ─────────────────────────────────────────────────────────────────────────────────────────────────
177 call `t = (b, a)`. Then, we check all the assumptions of this theorem and we apply it. -/
st ────────────────────────────────────────────────────────────────────────────────────────────
178 obtain ⟨b, ba, sab⟩ : ∃ b ∈ Iio a, Ico b a ⊆ s :=
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └────────────────────┘┴└───┘└─┘┴ ┴┴└─┘┴ ┴ ┴┴┴ └───
typ └────────────────────┘┴└───┘└─┘┴ ┴┴└─┘┴ ┴┴┴┴┴┴└───
doc └────────────────────┘ └───┘└─┘┴ ┴└─┘┴ ┴ ┴ ┴ └───
txt └────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └──────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────────────────
179 mem_nhds_within_Iio_iff_exists_Ico_subset.1 hs,
id └───────────────────────────────────────┘ └┘
src ───┘└───────────────────────────────────────┘└─┘
typ ───┘└───────────────────────────────────────┘└─┘└┘
doc ───┘└───────────────────────────────────────┘└─┘
txt ───┘ └─┘
par ───┘ └─┘
pid ───┘ └─┘
st ─────────────────────────────────────────────────┘└─
180 let t := Ioo b a,
id └─┘ ┴ ┴
src └───────┘└─┘┴ ┴
typ └───────┘└─┘┴┴┴┴
doc └───────┘└─┘┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴
st ─────────────────┘└─
181 have ts : t ⊆ s := subset.trans Ioo_subset_Ico_self sab,
id ┴ ┴ └──────────┘ └─────────────────┘ └─┘
src └────────┘ ┴ ┴ └──┘└──────────┘┴└─────────────────┘┴
typ └────────┘┴┴ ┴┴└──┘└──────────┘┴└─────────────────┘┴└─┘
doc └────────┘ ┴ ┴ └──┘ ┴ ┴
txt └────────┘ ┴ ┴ └──┘ ┴ ┴
par └────────┘ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
182 have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
id └───────────────┘ ┴ ┴ └─────────┘ └┘
src └────────────┘└───────────────┘┴ ┴ ┴ └──┘└─────────┘┴
typ └────────────┘└───────────────┘┴ ┴┴┴┴└──┘└─────────┘┴└┘
doc └────────────┘└───────────────┘┴ ┴ ┴ └──┘ ┴
txt └────────────┘ ┴ ┴ ┴ └──┘ ┴
par └────────────┘ ┴ ┴ ┴ └──┘ ┴
pid └─────────┘└─┘ ┴ ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────┘└─
183 have t_conv : convex t := convex_Ioo b a,
id └────┘ ┴ └────────┘ ┴ ┴
src └────────────┘└────┘┴ └──┘└────────┘┴ ┴
typ └────────────┘└────┘┴┴└──┘└────────┘┴┴┴┴
doc └────────────┘└────┘┴ └──┘ ┴ ┴
txt └────────────┘ ┴ └──┘ ┴ ┴
par └────────────┘ ┴ └──┘ ┴ ┴
pid └─────────┘└─┘ ┴ └──┘ ┴ ┴
st ─────────────────────────────────────────┘└─
184 have t_open : is_open t := is_open_Ioo,
id └─────┘ ┴ └─────────┘
src └────────────┘└─────┘┴ └──┘└─────────┘
typ └────────────┘└─────┘┴┴└──┘└─────────┘
doc └────────────┘└─────┘┴ └──┘
txt └────────────┘ ┴ └──┘
par └────────────┘ ┴ └──┘
pid └─────────┘└─┘ ┴ └──┘
st ───────────────────────────────────────┘└─
185 have t_closure : closure t = Icc b a := closure_Ioo ba,
id └─────┘ ┴ ┴ └─┘ ┴ ┴ └─────────┘ └┘
src └───────────────┘└─────┘┴ ┴┴┴└─┘┴ ┴ └──┘└─────────┘┴
typ └───────────────┘└─────┘┴┴┴┴┴└─┘┴┴┴┴└──┘└─────────┘┴└┘
doc └───────────────┘└─────┘┴ ┴ ┴└─┘┴ ┴ └──┘└─────────┘┴
txt └───────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────────────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────┘└─
186 have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
id └─────┘ └──────────────────┘ ┴ ┴
src └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴
typ └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴┴┴┴┴
doc └────────────┘ └──┘└─────┘┴ ┴└──────────────────┘┴ ┴ ┴
txt └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴
par └────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴
pid └─────────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
187 { rw t_closure,
id └───────┘
src └─┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└──────────┘└─
188 assume y hy,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
189 by_cases h : y = a,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
190 { rw h, exact f_lim.mono ts },
id ┴ └────────┘ └┘
src └─┘ └────┘└────────┘┴ ┴
typ └─┘┴ └────┘└────────┘┴└┘┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└──┘└────────────────────┘└┘└
191 { have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩,
id ┴ ┴ └─┘ └────────────┘ └┘ ┴
src └─────┘ ┴ ┴ └──┘ ┴ └──┘└────────────┘┴ └─┘ ┴
typ └─────┘┴┴ ┴┴└──┘└─┘┴ └──┘└────────────┘┴└┘└─┘┴┴
doc └─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴
par └─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴
st ──────────────────────────────────────────────────────┘└─
192 exact (f_diff.continuous_on y this).mono ts } },
id └──────────────────┘ ┴ └──┘ └┘
src └────┘ └──────────────────┘┴ ┴ └─────┘ ┴
typ └────┘ └──────────────────┘┴┴┴└──┘└─────┘└┘┴
doc └────┘ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ └─────┘ ┴
st ─────────────────────────────────────────────────┘└──┘└
193 have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
id └─────┘ └────┘ ┴ └─────────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ └────────┘└─┘ └┘
typ └─────────────┘└─────┘┴ └─┘└────┘┴ ┴┴┴ └┘ └─────────┘┴┴┴┴└┘ ┴┴ └────────┘└─┘┴└┘
doc └─────────────┘└─────┘┴ └─┘└────┘┴ ┴ ┴ └┘ └─────────┘┴ ┴ └┘ ┴┴ └────────┘└─┘ └┘
txt └─────────────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
par └─────────────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
pid └──────────┘└─┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └┘
st ─────────────────────────────────────────────────────────────────────────────────┘└─
194 { simp [deriv_fderiv.symm],
src └────┘ ┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───┘└──────────────────────┘└─
195 refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
id └──────────┘ └───────────────────────────────────────────────────────────────┘
src └─────┘└──────────┘┴└───────────────────────────────────────────────────────────────┘└┘
typ └─────┘└──────────┘┴└───────────────────────────────────────────────────────────────┘└┘
doc └─────┘ ┴└───────────────────────────────────────────────────────────────┘└┘
txt └─────┘ ┴ └┘
par └─────┘ ┴ └┘
pid ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
196 exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' },
id └─────────────┘ └──────────────┘ └─────────────────┘ └────┘
src └────┘└─────────────┘┴ └──────────────┘└─┘└─────────────────┘└┘ ┴
typ └────┘└─────────────┘┴ └──────────────┘└─┘└─────────────────┘└┘└────┘┴
doc └────┘ ┴ └─┘ └┘ ┴
txt └────┘ ┴ └─┘ └┘ ┴
par └────┘ ┴ └─┘ └┘ ┴
pid ┴ ┴ └─┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
197 -- now we can apply `has_fderiv_at_boundary_of_differentiable`
st ─────────────────────────────────────────────────────────────────
198 have : has_deriv_within_at f e (Icc b a) a,
id └─────────────────┘ ┴ ┴ └─┘ ┴ ┴
src └─────┘└─────────────────┘┴ ┴ ┴ └─┘┴ ┴ └┘
typ └─────┘└─────────────────┘┴┴┴┴┴ └─┘┴┴┴ └┘┴
doc └─────┘└─────────────────┘┴ ┴ ┴ └─┘┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
199 { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],
id └──────────────────────────────────────────┘ └───────┘
src └──┘└──────────────────────────────────────────┘└──┘ ┴
typ └──┘└──────────────────────────────────────────┘└──┘└───────┘┴
doc └──┘└──────────────────────────────────────────┘└──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ───┘└──────────────────────────────────────────────┘└───────────┘└──
200 exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff' },
id └──────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └─────┘
src └────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴
typ └────┘└──────────────────────────────────────┘┴└────┘┴└────┘┴└────┘┴└────┘┴└─────┘┴
doc └────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└┘└
201 exact this.nhds_within (mem_nhds_within_Iic_iff_exists_Icc_subset.2 ⟨b, ba, subset.refl _⟩)
id └──────────────┘ └───────────────────────────────────────┘ ┴ └┘ └─────────┘
src └────┘└──────────────┘┴ └───────────────────────────────────────┘└─┘ └┘ └┘└─────────┘└───┘
typ └────┘└──────────────┘┴ └───────────────────────────────────────┘└─┘ ┴└┘└┘└┘└─────────┘└───┘
doc └────┘ ┴ └───────────────────────────────────────┘└─┘ └┘ └┘ └───┘
txt └────┘ ┴ └─┘ └┘ └┘ └───┘
par └────┘ ┴ └─┘ └┘ └┘ └───┘
pid ┴ ┴ └─┘ └┘ └┘ └──┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────────┘
202 end
st └─┘